top(sent(x)) → top(check(rest(x)))
rest(nil) → sent(nil)
rest(cons(x, y)) → sent(y)
check(sent(x)) → sent(check(x))
check(rest(x)) → rest(check(x))
check(cons(x, y)) → cons(check(x), y)
check(cons(x, y)) → cons(x, check(y))
check(cons(x, y)) → cons(x, y)
↳ QTRS
↳ DependencyPairsProof
top(sent(x)) → top(check(rest(x)))
rest(nil) → sent(nil)
rest(cons(x, y)) → sent(y)
check(sent(x)) → sent(check(x))
check(rest(x)) → rest(check(x))
check(cons(x, y)) → cons(check(x), y)
check(cons(x, y)) → cons(x, check(y))
check(cons(x, y)) → cons(x, y)
TOP(sent(x)) → REST(x)
CHECK(cons(x, y)) → CHECK(y)
TOP(sent(x)) → CHECK(rest(x))
TOP(sent(x)) → TOP(check(rest(x)))
CHECK(sent(x)) → CHECK(x)
CHECK(rest(x)) → CHECK(x)
CHECK(cons(x, y)) → CHECK(x)
CHECK(rest(x)) → REST(check(x))
top(sent(x)) → top(check(rest(x)))
rest(nil) → sent(nil)
rest(cons(x, y)) → sent(y)
check(sent(x)) → sent(check(x))
check(rest(x)) → rest(check(x))
check(cons(x, y)) → cons(check(x), y)
check(cons(x, y)) → cons(x, check(y))
check(cons(x, y)) → cons(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
TOP(sent(x)) → REST(x)
CHECK(cons(x, y)) → CHECK(y)
TOP(sent(x)) → CHECK(rest(x))
TOP(sent(x)) → TOP(check(rest(x)))
CHECK(sent(x)) → CHECK(x)
CHECK(rest(x)) → CHECK(x)
CHECK(cons(x, y)) → CHECK(x)
CHECK(rest(x)) → REST(check(x))
top(sent(x)) → top(check(rest(x)))
rest(nil) → sent(nil)
rest(cons(x, y)) → sent(y)
check(sent(x)) → sent(check(x))
check(rest(x)) → rest(check(x))
check(cons(x, y)) → cons(check(x), y)
check(cons(x, y)) → cons(x, check(y))
check(cons(x, y)) → cons(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
CHECK(cons(x, y)) → CHECK(y)
CHECK(sent(x)) → CHECK(x)
CHECK(rest(x)) → CHECK(x)
CHECK(cons(x, y)) → CHECK(x)
top(sent(x)) → top(check(rest(x)))
rest(nil) → sent(nil)
rest(cons(x, y)) → sent(y)
check(sent(x)) → sent(check(x))
check(rest(x)) → rest(check(x))
check(cons(x, y)) → cons(check(x), y)
check(cons(x, y)) → cons(x, check(y))
check(cons(x, y)) → cons(x, y)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
CHECK(cons(x, y)) → CHECK(y)
CHECK(sent(x)) → CHECK(x)
CHECK(rest(x)) → CHECK(x)
CHECK(cons(x, y)) → CHECK(x)
The value of delta used in the strict ordering is 8.
POL(cons(x1, x2)) = 2 + (4)x_1 + x_2
POL(CHECK(x1)) = (4)x_1
POL(sent(x1)) = 3 + x_1
POL(rest(x1)) = 4 + (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
top(sent(x)) → top(check(rest(x)))
rest(nil) → sent(nil)
rest(cons(x, y)) → sent(y)
check(sent(x)) → sent(check(x))
check(rest(x)) → rest(check(x))
check(cons(x, y)) → cons(check(x), y)
check(cons(x, y)) → cons(x, check(y))
check(cons(x, y)) → cons(x, y)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
TOP(sent(x)) → TOP(check(rest(x)))
top(sent(x)) → top(check(rest(x)))
rest(nil) → sent(nil)
rest(cons(x, y)) → sent(y)
check(sent(x)) → sent(check(x))
check(rest(x)) → rest(check(x))
check(cons(x, y)) → cons(check(x), y)
check(cons(x, y)) → cons(x, check(y))
check(cons(x, y)) → cons(x, y)